In recent years, as information processing society has developed, a software system has penetrated general society, and very high reliability has been required in software. Meanwhile, software has been complicated and increased in size due to differential and derivative development, and a decrease in maintainability such as easy extension and easy understanding of software has become a problem.
Refactoring is a method disclosed in Non-Patent Documents 1 to 3, is a general term of a technique of improving a design quality of software by changing an internal structure without changing behavior of software, and reduces complexity and improves maintainability. The refactoring technique is a desired technique for securing maintainability of software that has been complicated and increased in size, but it is likely to lead to a new error since a source code is changed. Specifically, in the refactoring, there are methods classified as a plurality of patterns, and a change process of a source code and a condition for a source code for guaranteeing that behavior of software does not change by the change are explicitly or implicitly decided. When the source code is changed without following the change process or when the source code is changed without following the condition, since it is not guaranteed that behavior of software serving as a target does not change, an error is likely to occur in software. Thus, in a maintenance phase of software, a software developer may think that the refactoring may cause an error in software which is properly operating and thus decide not to perform the refactoring. For this reason, in the maintenance phase of software, in order to perform the refactoring actively, a technique of verifying that the refactoring causes no error is necessary.
In Non-Patent Document 3, 72 types of patterns of the refactoring (hereinafter, referred to simply as “refactoring patterns”) which are typically used are defined.
In the present specification, when two source codes are identical in external behavior, that is, obtain the same output for the same input at the time of execution, both source codes are defined as being “equivalent,” and verifying whether or not a source code before refactoring execution is equivalent to a source code after refactoring execution is referred to as “equivalence verification.”
Conditions required by a technique of verifying whether or not the source code before refactoring execution is equivalent to the source code after refactoring execution include the following conditions.
(1) One condition is that most of the work has to be automated, and a manual work has to be small. In the past, equivalence of a source code has been verified by manual review or test. By implementing automatic verification by a tool, verification manhours are reduced, and the refactoring is promoted.
(2) Another condition is that when behaviors are determined to be equivalent or non-equivalent by the refactoring verification technique, information serving as a ground therefore has to be presented to the developer. By presenting information serving as a determination criterion to be easily understood by the developer, the developer can perform re-verification, reliability of a tool is improved, and the refactoring is promoted.
Examples of an equivalence verification technique include a technique disclosed in Patent Document 1 that tests portions that are determined to be different by a source code comparison and compares results thereof, a technique disclosed in Non-Patent Document 1 that represents a source code using a graph and verifies whether or not a graph satisfies a pre-condition that is decided for each refactoring, and technique disclosed in Non-Patent Document 2 that verifies whether or not behaviors are being held using symbolic execution.